| Definitions |  x:A. B(x), s = t, x:A  B(x), t  T, x:A B(x), M1  M2, MsgA, , mk-ma, Id, IdDeq, lexpr{i}, Knd,   x. t(x), Type, KindDeq, <a,b>, locl(a), Prop, State(ds), f g, Valtype(da;k), 1of(t), f(x)?z, rcv(l,tg), 2of(t), x.A(x), Void, IdLnk, a:A fp B(a), type List, Top, S  T, S  T, strong-subtype(A;B), left+right,  x:A. B(x), Atom,  , {x:A| B(x) },  , A B,  A, False, a<b, #$n, EqDecider(T), x(s), f(a),  T, True, product-deq(A;B;a;b), IdLnkDeq, P   Q, P & Q, P  Q, P Q |